;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(interface Imirroring
  (sig mirror (tr orientation))
  
  (con mirror-vertical-returns-true-bmp-tree
       (implies (bmp-tree? tr)) 
       (true-bmp-tree? (mirror tr "vertical")))
  
  (con mirror-horizontal-returns-true-bmp-tree
       (implies (bmp-tree? tr)) 
       (true-bmp-tree? (mirror tr "horizontal")))
  
  (con mirror-vertical-round-trip
       (implies (bmp-tree? tr))
       (equal tr (mirror (mirror tr "vertical") "vertical")))
  
  (con mirror-horizontal-round-trip
       (implies (bmp-tree? tr))
       (equal tr (mirror (mirror tr "horizontal") "horizontal")))
  )